(set-info :smt-lib-version 2.5)
(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes () ((a0(c0$0)(c0$1)(c0$2)(c0$3)(c0$4)(c0$5(c0$5$0 aa)(c0$5$1 a3))(c0$6)(c0$7)(c0$8(c0$8$0 a8)(c0$8$1 ae)(c0$8$2 a13))(c0$9)(c0$a)(c0$b)(c0$c)(c0$d)(c0$e)(c0$f)(c0$10)(c0$11)(c0$12)(c0$13)(c0$14)(c0$15)(c0$16)(c0$17)(c0$18)(c0$19)(c0$1a)(c0$1b)(c0$1c)(c0$1d)(c0$1e))
                       (a1(c1$0(c1$0$0 a5)(c1$0$1 a8))(c1$1)(c1$2)(c1$3)(c1$4(c1$4$0 a3)(c1$4$1 a3)(c1$4$2 a5)(c1$4$3 a7)(c1$4$4 Int)(c1$4$5 ac)(c1$4$6 a13)(c1$4$7 ad)(c1$4$8 a4)(c1$4$9 a11)(c1$4$a Int)(c1$4$b aa)(c1$4$c Int)(c1$4$d a4))(c1$5)(c1$6)(c1$7)(c1$8)(c1$9)(c1$a)(c1$b(c1$b$0 a18))(c1$c)(c1$d))
                       (a2(c2$0)(c2$1)(c2$2(c2$2$0 a7)(c2$2$1 a2)(c2$2$2 a3)(c2$2$3 a12)(c2$2$4 Int)(c2$2$5 Bool)(c2$2$6 a18)(c2$2$7 a6)(c2$2$8 a1)(c2$2$9 a5)(c2$2$a ad)(c2$2$b a0)(c2$2$c a9)(c2$2$d a11)(c2$2$e a5)(c2$2$f a16)(c2$2$10 a13))(c2$3)(c2$4)(c2$5)(c2$6(c2$6$0 a1)(c2$6$1 a17)(c2$6$2 a15))(c2$7(c2$7$0 a2)(c2$7$1 a18)(c2$7$2 a16)(c2$7$3 a14))(c2$8)(c2$9)(c2$a)(c2$b)(c2$c)(c2$d)(c2$e))
                       (a3(c3$0)(c3$1)(c3$2)(c3$3(c3$3$0 a2)(c3$3$1 Int)(c3$3$2 a5)(c3$3$3 a6)(c3$3$4 a18)(c3$3$5 ab)(c3$3$6 a16)(c3$3$7 a6)(c3$3$8 a16))(c3$4(c3$4$0 a3)(c3$4$1 a8)(c3$4$2 a5)(c3$4$3 a15)(c3$4$4 a11)(c3$4$5 a15)(c3$4$6 a4)(c3$4$7 af)(c3$4$8 a5)(c3$4$9 a5)(c3$4$a Int)(c3$4$b ab)(c3$4$c a15)(c3$4$d ae))(c3$5)(c3$6)(c3$7)(c3$8)(c3$9))
                       (a4(c4$0)(c4$1)(c4$2)(c4$3)(c4$4)(c4$5)(c4$6)(c4$7)(c4$8(c4$8$0 a0)(c4$8$1 a9)(c4$8$2 a0)(c4$8$3 Int)(c4$8$4 a4)(c4$8$5 a16))(c4$9)(c4$a)(c4$b)(c4$c)(c4$d)(c4$e)(c4$f)(c4$10)(c4$11)(c4$12)(c4$13)(c4$14)(c4$15)(c4$16)(c4$17)(c4$18)(c4$19)(c4$1a)(c4$1b)(c4$1c)(c4$1d)(c4$1e)(c4$1f)(c4$20)(c4$21))
                       (a5(c5$0(c5$0$0 a18)(c5$0$1 a11)(c5$0$2 aa)(c5$0$3 ad)(c5$0$4 ad)(c5$0$5 ac)(c5$0$6 a7)(c5$0$7 Int)(c5$0$8 Int)(c5$0$9 a2)(c5$0$a Int)(c5$0$b a1)(c5$0$c ab)(c5$0$d a16)(c5$0$e a16)(c5$0$f a3))(c5$1(c5$1$0 a2)(c5$1$1 a4)(c5$1$2 Int)(c5$1$3 a0)(c5$1$4 a4)(c5$1$5 a0)(c5$1$6 a4)(c5$1$7 a4)(c5$1$8 a0)(c5$1$9 a4)(c5$1$a a0)(c5$1$b a3)(c5$1$c Int)(c5$1$d Int)(c5$1$e a0)(c5$1$f a1)(c5$1$10 a4)(c5$1$11 Int)))
                       (a6(c6$0)(c6$1)(c6$2(c6$2$0 a12)(c6$2$1 a8))(c6$3)(c6$4(c6$4$0 a8)(c6$4$1 Int)(c6$4$2 ad)(c6$4$3 aa)(c6$4$4 a10)(c6$4$5 a17)(c6$4$6 a11)(c6$4$7 Int)(c6$4$8 a18)(c6$4$9 a13)(c6$4$a ae)(c6$4$b a5)(c6$4$c Int)(c6$4$d Int)(c6$4$e a5)(c6$4$f ad)(c6$4$10 a10)(c6$4$11 a8)(c6$4$12 Int)(c6$4$13 a7)(c6$4$14 ac)(c6$4$15 a12)(c6$4$16 Int)(c6$4$17 a8)(c6$4$18 a18)(c6$4$19 Int)(c6$4$1a a15)(c6$4$1b a16))(c6$5)(c6$6)(c6$7)(c6$8)(c6$9)(c6$a)(c6$b)(c6$c(c6$c$0 a15)(c6$c$1 a3)(c6$c$2 ae))(c6$d)(c6$e)(c6$f)(c6$10)(c6$11)(c6$12)(c6$13)(c6$14)(c6$15)(c6$16)(c6$17)(c6$18)(c6$19)(c6$1a)(c6$1b))
                       (a7(c7$0(c7$0$0 ab)(c7$0$1 ad)(c7$0$2 a8)(c7$0$3 a0))(c7$1(c7$1$0 a1)(c7$1$1 a5)(c7$1$2 a5)(c7$1$3 Int)(c7$1$4 a10)(c7$1$5 a6)(c7$1$6 a16)(c7$1$7 a0)(c7$1$8 ab))(c7$2(c7$2$0 Int)(c7$2$1 a4)(c7$2$2 a0)(c7$2$3 a6)(c7$2$4 a5)(c7$2$5 a6)(c7$2$6 a6)(c7$2$7 a4)(c7$2$8 Bool)(c7$2$9 a0)(c7$2$a a4)(c7$2$b a1)(c7$2$c a6)(c7$2$d a3)(c7$2$e a0)(c7$2$f a1)(c7$2$10 a6)(c7$2$11 Int)))
                       (a8(c8$0)(c8$1)(c8$2(c8$2$0 ad)(c8$2$1 a13)(c8$2$2 a14)(c8$2$3 ae)(c8$2$4 a10)(c8$2$5 a16)(c8$2$6 a12)(c8$2$7 a10)(c8$2$8 a15)(c8$2$9 a3)(c8$2$a ae)(c8$2$b a7)(c8$2$c a13)(c8$2$d a17)(c8$2$e a8)(c8$2$f ac)(c8$2$10 a2)(c8$2$11 Int)(c8$2$12 a16))(c8$3(c8$3$0 a15)(c8$3$1 a3))(c8$4)(c8$5)(c8$6)(c8$7)(c8$8)(c8$9(c8$9$0 a4)(c8$9$1 a12)(c8$9$2 a2))(c8$a)(c8$b))
                       (a9(c9$0)(c9$1)(c9$2)(c9$3(c9$3$0 a5))(c9$4)(c9$5(c9$5$0 a4)(c9$5$1 a8)(c9$5$2 af)(c9$5$3 a0)(c9$5$4 a6)(c9$5$5 a3)(c9$5$6 ad)(c9$5$7 a7)(c9$5$8 a12)(c9$5$9 a0)(c9$5$a a7)(c9$5$b ad)(c9$5$c Int)(c9$5$d a5)(c9$5$e ae)(c9$5$f a9)(c9$5$10 a7)(c9$5$11 a11)(c9$5$12 a13)(c9$5$13 a7)(c9$5$14 Bool)(c9$5$15 Int)(c9$5$16 a5)(c9$5$17 a11)(c9$5$18 a5)(c9$5$19 a11)(c9$5$1a a2)(c9$5$1b a4)(c9$5$1c a10)(c9$5$1d a11)(c9$5$1e a14)(c9$5$1f a10))(c9$6)(c9$7)(c9$8)(c9$9)(c9$a)(c9$b)(c9$c)(c9$d))
                       (aa(ca$0)(ca$1)(ca$2(ca$2$0 a6)(ca$2$1 a0))(ca$3)(ca$4(ca$4$0 a18)(ca$4$1 Int)(ca$4$2 ab)(ca$4$3 a2)(ca$4$4 a0)(ca$4$5 ad)(ca$4$6 a8)(ca$4$7 a12)(ca$4$8 Bool)(ca$4$9 a5)(ca$4$a a5)(ca$4$b a15))(ca$5)(ca$6)(ca$7)(ca$8)(ca$9)(ca$a)(ca$b)(ca$c)(ca$d)(ca$e)(ca$f)(ca$10(ca$10$0 a6)(ca$10$1 a0)(ca$10$2 a18))(ca$11)(ca$12)(ca$13))
                       (ab(cb$0(cb$0$0 a14)(cb$0$1 aa)(cb$0$2 ac)(cb$0$3 a10)(cb$0$4 a9)(cb$0$5 a13)(cb$0$6 a15)(cb$0$7 a14)(cb$0$8 a0)(cb$0$9 Int)(cb$0$a Bool)(cb$0$b aa)(cb$0$c Bool)(cb$0$d a3)(cb$0$e af)(cb$0$f a16)(cb$0$10 a13)(cb$0$11 Int)(cb$0$12 a2)(cb$0$13 aa))(cb$1(cb$1$0 a0)(cb$1$1 a0)(cb$1$2 a2)(cb$1$3 a0)(cb$1$4 Int)))
                       (ac(cc$0(cc$0$0 a17)(cc$0$1 a0))(cc$1)(cc$2)(cc$3)(cc$4(cc$4$0 a8)(cc$4$1 a9)(cc$4$2 aa)(cc$4$3 a7)(cc$4$4 a1)(cc$4$5 ac)(cc$4$6 Int)(cc$4$7 aa)(cc$4$8 a13)(cc$4$9 a17)(cc$4$a ac)(cc$4$b Int)(cc$4$c a17)(cc$4$d a3)(cc$4$e Int)(cc$4$f a17)(cc$4$10 a12)(cc$4$11 aa)(cc$4$12 a15)(cc$4$13 a6)(cc$4$14 a12)(cc$4$15 ac))(cc$5(cc$5$0 a5)(cc$5$1 a4)(cc$5$2 a3)(cc$5$3 ae))(cc$6)(cc$7)(cc$8(cc$8$0 a3))(cc$9)(cc$a)(cc$b)(cc$c(cc$c$0 a9))(cc$d)(cc$e))
                       (ad(cd$0)(cd$1)(cd$2)(cd$3(cd$3$0 aa)(cd$3$1 a16)(cd$3$2 Int)(cd$3$3 a8)(cd$3$4 Int)(cd$3$5 a5)(cd$3$6 Int)(cd$3$7 ac)(cd$3$8 a1)(cd$3$9 ab)(cd$3$a af)(cd$3$b a2)(cd$3$c a1)(cd$3$d a15)(cd$3$e a16)(cd$3$f a2)(cd$3$10 ab)(cd$3$11 a6)(cd$3$12 a13))(cd$4)(cd$5)(cd$6)(cd$7)(cd$8)(cd$9(cd$9$0 a8)(cd$9$1 ad))(cd$a)(cd$b)(cd$c)(cd$d)(cd$e)(cd$f)(cd$10)(cd$11)(cd$12)(cd$13))
                       (ae(ce$0(ce$0$0 a9))(ce$1(ce$1$0 a14)(ce$1$1 a3)(ce$1$2 a0)(ce$1$3 a15)(ce$1$4 a8)(ce$1$5 ad)(ce$1$6 a11)(ce$1$7 af)(ce$1$8 a17)(ce$1$9 a7)(ce$1$a a11)(ce$1$b ad)(ce$1$c a3)(ce$1$d a17)(ce$1$e a14)(ce$1$f af)(ce$1$10 a6)(ce$1$11 a0))(ce$2)(ce$3)(ce$4)(ce$5)(ce$6)(ce$7)(ce$8)(ce$9)(ce$a)(ce$b)(ce$c(ce$c$0 a5)(ce$c$1 a7)(ce$c$2 a12)(ce$c$3 Bool)(ce$c$4 a6)(ce$c$5 aa)(ce$c$6 a12)(ce$c$7 a7)(ce$c$8 a8)(ce$c$9 a5)(ce$c$a Int)(ce$c$b a8))(ce$d))
                       (af(cf$0)(cf$1)(cf$2)(cf$3)(cf$4)(cf$5)(cf$6)(cf$7)(cf$8)(cf$9)(cf$a)(cf$b)(cf$c)(cf$d(cf$d$0 a0)(cf$d$1 a12)(cf$d$2 a16)(cf$d$3 a16)(cf$d$4 ac)(cf$d$5 a8)(cf$d$6 ae)(cf$d$7 a10)(cf$d$8 a1)(cf$d$9 ad)(cf$d$a ac)(cf$d$b a2)(cf$d$c a15)(cf$d$d a3)(cf$d$e a1)(cf$d$f Int)(cf$d$10 a1)(cf$d$11 Int))(cf$e)(cf$f)(cf$10)(cf$11)(cf$12)(cf$13(cf$13$0 a17)(cf$13$1 a0)(cf$13$2 Int)(cf$13$3 a12)(cf$13$4 a0))(cf$14)(cf$15)(cf$16))
                       (a10(c10$0)(c10$1)(c10$2)(c10$3)(c10$4)(c10$5)(c10$6(c10$6$0 ad)(c10$6$1 a0)(c10$6$2 aa)(c10$6$3 a0))(c10$7)(c10$8)(c10$9)(c10$a)(c10$b)(c10$c)(c10$d)(c10$e)(c10$f)(c10$10)(c10$11)(c10$12)(c10$13)(c10$14)(c10$15))
                       (a11(c11$0(c11$0$0 a0))(c11$1)(c11$2)(c11$3(c11$3$0 a5)(c11$3$1 a16)(c11$3$2 a2)(c11$3$3 ae)(c11$3$4 ab)(c11$3$5 a15)(c11$3$6 af)(c11$3$7 a1)(c11$3$8 a6)(c11$3$9 a12)(c11$3$a a14)(c11$3$b a13)(c11$3$c a18)(c11$3$d a16)(c11$3$e Bool)(c11$3$f aa)(c11$3$10 a1)(c11$3$11 a13))(c11$4)(c11$5)(c11$6)(c11$7)(c11$8)(c11$9)(c11$a)(c11$b)(c11$c(c11$c$0 a17)(c11$c$1 a0)(c11$c$2 a9)(c11$c$3 ad)(c11$c$4 a17)(c11$c$5 a18)(c11$c$6 Int))(c11$d)(c11$e)(c11$f)(c11$10)(c11$11)(c11$12)(c11$13(c11$13$0 ad)(c11$13$1 a1)(c11$13$2 a12)(c11$13$3 a11))(c11$14)(c11$15)(c11$16)(c11$17)(c11$18)(c11$19)(c11$1a))
                       (a12(c12$0)(c12$1)(c12$2)(c12$3)(c12$4(c12$4$0 ad)(c12$4$1 a2)(c12$4$2 af)(c12$4$3 a9)(c12$4$4 a18)(c12$4$5 a17)(c12$4$6 a9)(c12$4$7 a1))(c12$5)(c12$6)(c12$7(c12$7$0 a17)(c12$7$1 a12)(c12$7$2 Bool)(c12$7$3 a4)(c12$7$4 a10)(c12$7$5 a2)(c12$7$6 a18)(c12$7$7 a0)(c12$7$8 a9)(c12$7$9 a16)(c12$7$a a3)(c12$7$b ac)(c12$7$c a11)(c12$7$d ad)(c12$7$e Int)(c12$7$f af))(c12$8)(c12$9)(c12$a)(c12$b)(c12$c)(c12$d)(c12$e)(c12$f)(c12$10)(c12$11)(c12$12(c12$12$0 aa))(c12$13)(c12$14)(c12$15)(c12$16)(c12$17)(c12$18)(c12$19)(c12$1a)(c12$1b)(c12$1c)(c12$1d)(c12$1e)(c12$1f)(c12$20))
                       (a13(c13$0)(c13$1)(c13$2)(c13$3)(c13$4(c13$4$0 a14)(c13$4$1 a17)(c13$4$2 a13)(c13$4$3 a2)(c13$4$4 a3)(c13$4$5 a12)(c13$4$6 ac)(c13$4$7 a15)(c13$4$8 Int)(c13$4$9 ab)(c13$4$a a8)(c13$4$b a0)(c13$4$c a4)(c13$4$d a2)(c13$4$e a6)(c13$4$f ae)(c13$4$10 Int)(c13$4$11 Int)(c13$4$12 a18)(c13$4$13 a5)(c13$4$14 a10)(c13$4$15 ab)(c13$4$16 a18)(c13$4$17 a0)(c13$4$18 af)(c13$4$19 af))(c13$5)(c13$6)(c13$7)(c13$8)(c13$9)(c13$a)(c13$b)(c13$c)(c13$d)(c13$e)(c13$f)(c13$10))
                       (a14(c14$0)(c14$1)(c14$2)(c14$3)(c14$4)(c14$5)(c14$6)(c14$7)(c14$8)(c14$9)(c14$a)(c14$b)(c14$c)(c14$d)(c14$e)(c14$f)(c14$10)(c14$11)(c14$12)(c14$13)(c14$14))
                       (a15(c15$0)(c15$1)(c15$2)(c15$3)(c15$4)(c15$5(c15$5$0 ad)(c15$5$1 a6)(c15$5$2 a0)(c15$5$3 a12)(c15$5$4 a8)(c15$5$5 a3)(c15$5$6 a9)(c15$5$7 a0)(c15$5$8 Bool)(c15$5$9 a0)(c15$5$a ab)(c15$5$b a16)(c15$5$c a3)(c15$5$d a18)(c15$5$e ab)(c15$5$f ac))(c15$6)(c15$7)(c15$8)(c15$9)(c15$a)(c15$b)(c15$c(c15$c$0 a8)(c15$c$1 Int)(c15$c$2 a4)(c15$c$3 a12)(c15$c$4 a16)(c15$c$5 ab)(c15$c$6 a9)(c15$c$7 a18)(c15$c$8 a6)(c15$c$9 ac))(c15$d)(c15$e)(c15$f)(c15$10)(c15$11)(c15$12)(c15$13)(c15$14(c15$14$0 a5)(c15$14$1 a11))(c15$15)(c15$16)(c15$17)(c15$18)(c15$19))
                       (a16(c16$0)(c16$1)(c16$2)(c16$3)(c16$4)(c16$5)(c16$6(c16$6$0 a3)(c16$6$1 a15)(c16$6$2 a5)(c16$6$3 Int)(c16$6$4 a12)(c16$6$5 aa)(c16$6$6 Int)(c16$6$7 a0)(c16$6$8 a10)(c16$6$9 a18)(c16$6$a a13)(c16$6$b a4))(c16$7)(c16$8)(c16$9)(c16$a)(c16$b)(c16$c)(c16$d)(c16$e)(c16$f)(c16$10)(c16$11)(c16$12)(c16$13)(c16$14)(c16$15)(c16$16)(c16$17)(c16$18)(c16$19))
                       (a17(c17$0)(c17$1)(c17$2(c17$2$0 Int)(c17$2$1 a7)(c17$2$2 a16))(c17$3)(c17$4)(c17$5(c17$5$0 a18)(c17$5$1 a11)(c17$5$2 a9)(c17$5$3 a18)(c17$5$4 a15)(c17$5$5 a1)(c17$5$6 a6)(c17$5$7 a5)(c17$5$8 a3)(c17$5$9 ab)(c17$5$a a13)(c17$5$b a12)(c17$5$c a0)(c17$5$d a1)(c17$5$e ac)(c17$5$f a4)(c17$5$10 a8)(c17$5$11 Int)(c17$5$12 af)(c17$5$13 a6))(c17$6)(c17$7)(c17$8)(c17$9)(c17$a)(c17$b)(c17$c)(c17$d)(c17$e(c17$e$0 a17)(c17$e$1 a5)(c17$e$2 a18)(c17$e$3 a1)(c17$e$4 a11)(c17$e$5 Int)(c17$e$6 ab))(c17$f)(c17$10)(c17$11)(c17$12)(c17$13)(c17$14)(c17$15)(c17$16)(c17$17)(c17$18)(c17$19)(c17$1a))
                       (a18(c18$0(c18$0$0 ab))(c18$1)(c18$2(c18$2$0 Bool)(c18$2$1 a7)(c18$2$2 a17))(c18$3)(c18$4(c18$4$0 ab)(c18$4$1 a1)(c18$4$2 a11)(c18$4$3 Bool)(c18$4$4 a7)(c18$4$5 a2)(c18$4$6 a16)(c18$4$7 ab)(c18$4$8 a2)(c18$4$9 a18)(c18$4$a a6)(c18$4$b a16)(c18$4$c a7)(c18$4$d ad)(c18$4$e a3)(c18$4$f ad)(c18$4$10 a9)(c18$4$11 a2)(c18$4$12 a0)(c18$4$13 a16))(c18$5(c18$5$0 a3)(c18$5$1 af)(c18$5$2 a15)(c18$5$3 a8)(c18$5$4 a2)(c18$5$5 a11))(c18$6(c18$6$0 a7)))))

(push 1)
(declare-fun v0() a0)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$0 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$1 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$2 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$3 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$4 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$5 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$6 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$7 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$8 v0))
(check-sat)
;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$9 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$a v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$b v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$c v0))
;(check-sat)
;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$d v0))
;(check-sat)
;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$e v0))
;(check-sat)
;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$f v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$10 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$11 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$12 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$13 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$14 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$15 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$16 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$17 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
;(assert (is-c0$18 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$19 v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$1a v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$1b v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$1c v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$1d v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c0$1e v0))
;(check-sat)
;;(get-value (v0))
(pop 1)
(pop 1)
(push 1)
(declare-fun v1() a1)
;(get-info :name)
;(get-info :version)
(push 1)
(assert (is-c1$0 v1))
(check-sat)
